a, b, c, d:. ((c = 0  ))  ((d = 0  ))  (((a/c) * (b/d)) = (a * b/c * d)  ) 

latex

Definitions	T, P & Q, P  Q, P  Q, True, P  Q, , t  T, A, P  Q, x:A. B(x), False, S  T
Lemmas	qmul-qdiv-cancel2, qmul-qdiv-cancel, true wf, squash wf, qmul ac 1 qrng, qmul-qdiv-cancel3, qmul comm qrng, qdiv wf, qmul wf, qmul-preserves-eq, qmul-zero, not functionality wrt iff, int inc rationals, rationals wf, not wf